|
|
Approximate Techniques for Markov Models
Andriushchenko, Roman ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
In this work we discuss approximative techniques for the analysis of Markov chains, namely, state space aggregation and truncation. First, we focus on the application of the former method for the analysis of discrete-time models: we redesign the clustering algorithm to handle chains with an arbitrary structure of the state space and, most importantly, we improve upon existing bounds on the approximation error. The developed approach is then integrated with uniformisation techniques, in both standard and adaptive forms, to approximate continuous-time models as well as provide estimates of the approximation error. This theoretical framework along with existing truncation-based techniques were implemented within PRISM model checker. Experiments confirm that newly derived bounds provide a several orders of magnitude precision improvement without degrading performance. We show that the resulting aggregating approach can provide a valid model approximation supplied by adequate approximation error estimates, in both discrete and continuous time. Then, we perform a comparative analysis of aggregating and truncating techniques, illustrate how different methods handle various types of models, and identify chains for which aggregating, or truncating, analysis is preferred. Finally, we demonstrate a successful usage of approximative techniques for model checking Markov chains.
|
|
|
Synthesis of Probabilistic Programs with Rewards
Hranička, Vojtěch ; Síč, Juraj (referee) ; Češka, Milan (advisor)
This thesis pursues the synthesis of probabilistic programs with rewards. Probabilistic synthesis leads to the automatic proposal of a system which fulfills required specifications. In this thesis, I work with a form of synthesis where we have a sketch of a given system. This sketch includes unknown variables and the objective is to find a combination of configuration of given variables in order to have the final program meeting the specified requirements. Recently, new approaches considering a set of solutions as a family of Markov chain have appeared. One of these approaches is the usage of a new method combining counterexample-guided abstraction refinement and counterexample-guided inductive synthesis. This method exceeds other methods for synthesis of probabilistic programs with its efficiency. In this thesis, I concretely focus on extending this tool's specification language by adding a possibility of application of rewards and until properties. Thanks to these extensions it is possible to specify searched solution more efficiently. Experiments demonstrate that even after the addition of these possibilities of specifications the speed of a given tool remains by a margin of order of magnitudes more effective than the standard method of synthesis.
|
|
|
Computer-Aided Synthesis of Probabilistic Models
Andriushchenko, Roman ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
Předkládaná práce se zabývá problémem automatizované syntézy pravděpodobnostních systémů: máme-li rodinu Markovských řetězců, jak lze efektivně identifikovat ten který odpovídá zadané specifikaci? Takové rodiny často vznikají v nejrůznějších oblastech inženýrství při modelování systémů s neurčitostí a rozhodování i těch nejjednodušších syntézních otázek představuje NP-těžký problém. V dané práci my zkoumáme existující techniky založené na protipříklady řízené induktivní syntéze (counterexample-guided inductive synthesis, CEGIS) a na zjemňování abstrakce (counterexample-guided abstraction refinement, CEGAR) a navrhujeme novou integrovanou metodu pro pravděpodobnostní syntézu. Experimenty nad relevantními modely demonstrují, že navržená technika je nejenom srovnatelná s moderními metodami, ale ve většině případů dokáže výrazně překonat, někdy i o několik řádů, existující přístupy.
|
|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
|
|
Synthesis of Probabilistic Programs with Rewards
Hranička, Vojtěch ; Síč, Juraj (referee) ; Češka, Milan (advisor)
This thesis pursues the synthesis of probabilistic programs with rewards. Probabilistic synthesis leads to the automatic proposal of a system which fulfills required specifications. In this thesis, I work with a form of synthesis where we have a sketch of a given system. This sketch includes unknown variables and the objective is to find a combination of configuration of given variables in order to have the final program meeting the specified requirements. Recently, new approaches considering a set of solutions as a family of Markov chain have appeared. One of these approaches is the usage of a new method combining counterexample-guided abstraction refinement and counterexample-guided inductive synthesis. This method exceeds other methods for synthesis of probabilistic programs with its efficiency. In this thesis, I concretely focus on extending this tool's specification language by adding a possibility of application of rewards and until properties. Thanks to these extensions it is possible to specify searched solution more efficiently. Experiments demonstrate that even after the addition of these possibilities of specifications the speed of a given tool remains by a margin of order of magnitudes more effective than the standard method of synthesis.
|
|
|
Computer-Aided Synthesis of Probabilistic Models
Andriushchenko, Roman ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
Předkládaná práce se zabývá problémem automatizované syntézy pravděpodobnostních systémů: máme-li rodinu Markovských řetězců, jak lze efektivně identifikovat ten který odpovídá zadané specifikaci? Takové rodiny často vznikají v nejrůznějších oblastech inženýrství při modelování systémů s neurčitostí a rozhodování i těch nejjednodušších syntézních otázek představuje NP-těžký problém. V dané práci my zkoumáme existující techniky založené na protipříklady řízené induktivní syntéze (counterexample-guided inductive synthesis, CEGIS) a na zjemňování abstrakce (counterexample-guided abstraction refinement, CEGAR) a navrhujeme novou integrovanou metodu pro pravděpodobnostní syntézu. Experimenty nad relevantními modely demonstrují, že navržená technika je nejenom srovnatelná s moderními metodami, ale ve většině případů dokáže výrazně překonat, někdy i o několik řádů, existující přístupy.
|
|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
|
|
Approximate Techniques for Markov Models
Andriushchenko, Roman ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
In this work we discuss approximative techniques for the analysis of Markov chains, namely, state space aggregation and truncation. First, we focus on the application of the former method for the analysis of discrete-time models: we redesign the clustering algorithm to handle chains with an arbitrary structure of the state space and, most importantly, we improve upon existing bounds on the approximation error. The developed approach is then integrated with uniformisation techniques, in both standard and adaptive forms, to approximate continuous-time models as well as provide estimates of the approximation error. This theoretical framework along with existing truncation-based techniques were implemented within PRISM model checker. Experiments confirm that newly derived bounds provide a several orders of magnitude precision improvement without degrading performance. We show that the resulting aggregating approach can provide a valid model approximation supplied by adequate approximation error estimates, in both discrete and continuous time. Then, we perform a comparative analysis of aggregating and truncating techniques, illustrate how different methods handle various types of models, and identify chains for which aggregating, or truncating, analysis is preferred. Finally, we demonstrate a successful usage of approximative techniques for model checking Markov chains.
|
guest ::
